In many disciplines, such as aerodynamics, systems are modeled before finalizing the system design. The modeling of the system verifies that the system design satisfies functional and safety properties before the system is implemented. This modeling relies on mathematical analysis to verify all possible outcomes based on a set of allowed rules.
In contrast, currently, many software systems are verified by performing live testing, which means that the software systems are tested while they operate in a “real world” situation. When problems are identified, the software is modified to correct the problem. Once the software operates within a minimal acceptable reliability range, the live testing ends. Live testing is helpful in detecting major design flaws and certain programming errors. However, because it is nearly impossible to anticipate all the scenarios in which the software will operate and then test each scenario, the software will most likely still have errors after live testing.
Recently, there has been great interest in the possibility of modeling software systems. However, modeling software, which is an infinite-state system, becomes extremely difficult due to the state-space explosion problem associated with large systems. To overcome this problem, one approach constructs an abstract model of the software system, commonly referred to as a predicate abstraction. Based on the predicate abstraction, the concrete states of the software system are mapped to abstract states according to their evaluation under a finite set of predicates. While this technique is very useful, generating the predicate abstraction is very difficult. Currently, automatic predicate abstraction is performed on finite-state systems and on infinite-state systems with guarded commands. Both of these systems are restrictive in their application, and fall short of generating an automatic predicate abstraction on a program written using a general programming language, such as C and other industrial programming languages.